COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	\magnify{1100}
C00011 ENDMK
C⊗;
\magnify{1100}
\def\xskip{\hskip7pt plus3pt minus4pt}
\catcode`|=13
\def|#1|{\hbox{\it#1\/}}
\def\IF{\mathop{\bf if}}
\def\THEN{\mathrel{\bf then}}
\def\ELSE{\mathrel{\bf else}}
\def\AND{\mathrel{\bf and}}
\def\OR{\mathrel{\bf or}}
\def\NOT{\mathop{\bf not}}
\def\N{\mathop{\bf n}}
\def\T{\hbox{\tt T}}
\def\NIL{\hbox{\tt NIL}}
\def\.{\mathbin{.}}
\def\A{\mathop{\bf a}}
\def\D{\mathop{\bf d}}
\def\EQ{\mathrel{\bf eq}}
\def\AT{\mathop{\bf at}}
\def\quote#1{\hbox{\sfcode`.=1000\tt#1}}
\def\list#1{\langle#1\rangle}

\ctrline{\bf CS 206---Recursive Programming and Proving}
\vskip 20pt
\ctrline{Final Examination}
\ctrline{December 14, 1982}
\vskip 20pt
\parindent 0pt
\parskip 4pt
\def\prob#1.{\bigbreak #1.\quad\ignorespace}

This examination is open book and notes.  Either external or internal
notation may be used in writing LISP functions.  Each question on this
exam will be worth an equal amount, although they vary in difficulty.

\prob 1. 
We will say that a list $u$ is ``intermittently contained'' in a list $v$
if the elements of $u$ occur in $v$ in the same order as in $u$ but
possibly separated by other elements of $v$.  We write $u\preceq v$ for
this relation.  Thus we have
$$\quote{(A C E)}\preceq\quote{(X A B C A F D E G)}.$$
Write a recursive definition of $u\preceq v$.

\prob 2. 
$|partitions|\,n$ is a list of the partitions of the integer $n$ into sums
of smaller integers.  Thus,
$$\eqalign{|partitions|\,\quote{1}&=\quote{((1))},\cr
|partitions|\,\quote{2}&=\quote{((2) (1 1))},\cr
|partitions|\,\quote{3}&=\quote{((3) (2 1) (1 1 1))},\cr
|partitions|\,\quote{4}&=\quote{((4) (3 1) (2 2) (2 1 1) (1 1 1 1))}.\cr}$$
Write the function |partitions|.

\prob 3. 
The function $|insert|[n,u]$ inserts the integer $n$ into the list of integers
$u$, preserving ascending sequence in $u$.  Thus, for example,
$$\eqalign{|insert|[\quote{5},\quote{(-3 4 7 8)}]&=\quote{(-3 4 5 7 8)},\cr
|insert|[\quote{4},\quote{(2 4 5)}]&=\quote{(2 4 4 5)},\cr
|insert|[\quote{1},\quote{NIL}]&=\quote{(1)}.\cr}$$
\item{(a)} Write a pure LISP |insert| function.
\item{(b)} Write a version of |insert| which does destructive operations
    (i.e.\ |rplaca| and/or |rplacd|) and which uses only one cons-cell of
    list storage each time it is called.
\item{(c)} The following program uses |insert| to perform insertion sort:
    $$\eqalign{|sort|\,u ←\null&\IF\N u\THEN\NIL\cr
    &\ELSE|insert|[\A u,|sort|\,\D u]\cr}$$
    Prove $∀u.\,|isordered|\,|sort|\,u$, where
    $$\eqalign{|isordered|\,u ←\null&\N u\OR\N\D u\OR\cr
    &(\A u≤\A\D u\AND|isordered|\,\D u)\cr}$$
    You may assume that the version of |insert| called by |sort| is the pure
    LISP version that you wrote in part (a).
\item{(d)} What else would have to be proved in order to show that |sort| is
    a correct sorting function?

\prob 4. 
Write a macro {\tt PSETQ} which performs a ``parallel {\tt SETQ}'' operation.
The general use of this macro will be of the form
$$\quote{(PSETQ v1 e1 v2 e2 ...\ vn en)},$$
where each {\tt v}$i$ is a variable name (an atom), and each {\tt e}$i$
is an expression.  The result will be that of evaluating all of the
expressions {\tt e}$i$ (in order, since they could conceivably have side
effects), and then assigning them to the corresponding valiables {\tt v}$i$.
An example of the use of {\tt PSETQ} is
$$\quote{(psetq a b b a)},$$
which interchanges the values of {\tt a} and {\tt b}.\xskip ({\tt PSETQ} is
available in Lisp Machine Lisp and MacLisp, but you should not use this fact.)
You may assume that {\tt PSETQ} is always called with an even (and non-zero)
number of arguments.

\prob 5. 
Write an abstract evaluator |istrue| for Boolean expressions using the
abstract syntactic functions
\item{a.} $|isand|\,e$ meaning that $e$ has principal connective ``and''.
\item{b.} $|isor|\,e$ meaning that $e$ has principal connective ``or''.
\item{c.} $|isnot|\,e$ meaning that $e$ has principal connective ``not''.
\item{d.} In each of the three above cases, $|operands|\,e$ gives a list
of the operands of the expression.  If $e$ satisfies |isnot|, there is
exactly one operand, but in the other cases there may be any number.  The
LISP functions and predicates $\A$, $\D$, $\N$ are applicable to these lists.
\item{e.} $|isvar|\,e$ means that $e$ is a Boolean variable, and in this
case the predicate $|true|[e,\xi]$ is true if $e$ is true in the
state $\xi$.

Write a recursive definition of the predicate $|istrue|[e,\xi]$
whose value is true or false according to whether the Boolean expression
$e$ is true in the state $\xi$.  Your program should
not look at more terms of ``and''s and ``or''s than necessary to
decide the truth value.

\prob 6.
An S-expression $x$ is said to be |compact| if all {\tt EQUAL} subexpressions in
$x$ are {\tt EQ}.  Write a function $|compactify|[x,y]$ which is called with $x$
any S-expression and $y$ a compact S-expresion, and returns an S-expression that
is {\tt EQUAL} to $x$, is compact, and shares storage with $y$ as much as
possible.  Thus, whenever a subexpression of $x$ is {\tt EQUAL} to a
subexpression of $y$, the corresponding subexpression in the result will be
{\tt EQ} to that subexpression of $y$.

\vfill\end